Nuprl Lemma : qle_transitivity_qorder 11,40

a,b,c:rationals. qle(ab qle(bc qle(ac
latex


Definitionst  T, t.1, ocgrp{i:l}, qadd_grp, grp_car(g), x:AB(x), qle(rs)
Lemmasocgrp wf, qadd grp wf2, grp leq transitivity

origin